/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.Collection;
import java.util.Collections;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.WeakHashMap;

import org.eclipse.jdt.core.ICompilationUnit;
import org.eclipse.jdt.core.IJavaElement;
import org.eclipse.jdt.core.ITypeRoot;
import org.eclipse.jdt.core.dom.AST;
import org.eclipse.jdt.core.dom.ASTNode;
import org.eclipse.jdt.core.dom.ASTParser;
import org.eclipse.jdt.core.dom.ASTVisitor;
import org.eclipse.jdt.core.dom.Assignment;
import org.eclipse.jdt.core.dom.ClassInstanceCreation;
import org.eclipse.jdt.core.dom.CompilationUnit;
import org.eclipse.jdt.core.dom.ConstructorInvocation;
import org.eclipse.jdt.core.dom.DoStatement;
import org.eclipse.jdt.core.dom.EnhancedForStatement;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.FieldAccess;
import org.eclipse.jdt.core.dom.ForStatement;
import org.eclipse.jdt.core.dom.IAnnotationBinding;
import org.eclipse.jdt.core.dom.IBinding;
import org.eclipse.jdt.core.dom.IMemberValuePairBinding;
import org.eclipse.jdt.core.dom.IMethodBinding;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.MethodInvocation;
import org.eclipse.jdt.core.dom.Modifier;
import org.eclipse.jdt.core.dom.NumberLiteral;
import org.eclipse.jdt.core.dom.ParenthesizedExpression;
import org.eclipse.jdt.core.dom.QualifiedName;
import org.eclipse.jdt.core.dom.ReturnStatement;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.SingleVariableDeclaration;
import org.eclipse.jdt.core.dom.Statement;
import org.eclipse.jdt.core.dom.SuperConstructorInvocation;
import org.eclipse.jdt.core.dom.SuperMethodInvocation;
import org.eclipse.jdt.core.dom.ThisExpression;
import org.eclipse.jdt.core.dom.TypeDeclaration;
import org.eclipse.jdt.core.dom.VariableDeclaration;
import org.eclipse.jdt.core.dom.VariableDeclarationFragment;
import org.eclipse.jdt.core.dom.WhileStatement;

import com.googlecode.syper.anno.Excl;
import com.googlecode.syper.anno.Old;
import com.googlecode.syper.anno.Pred;
import com.googlecode.syper.anno.Result;
import com.googlecode.syper.javasyp.checker.ExpressionEncoder.Lookup;
import com.googlecode.syper.javasyp.formulae.Field;
import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.formulae.Local;
import com.googlecode.syper.javasyp.formulae.Pre;
import com.googlecode.syper.javasyp.formulae.Ref;
import com.googlecode.syper.javasyp.formulae.Select;

import edu.cmu.cs.crystal.annotations.AnnotationDatabase;
import edu.cmu.cs.crystal.annotations.AnnotationSummary;
import edu.cmu.cs.crystal.annotations.ICrystalAnnotation;

/**
 * @author kevin
 * @since Jan 31, 2010
 *
 */
public class ContractRegistry {

	private static final String SUPER_PREFIX = "super.";

	private static final SypContractLookup SYP_CONTRACT_LOOKUP_INSTANCE =
		new SypContractLookup();

	private final Map<IMethodBinding, Contract> contracts =
		new WeakHashMap<IMethodBinding, Contract>();
	protected AnnotationDatabase annos;

//	/**
//	 * Returns (possibly zero) pre-conditions declared for the given method
//	 * @param decl
//	 * @return pre-conditions declared for the given method, never {@code null}
//	 */
//	public static Iterable<Expression> getPre(MethodDeclaration decl) {
//		ContractFinder f = new ContractFinder();
//		decl.accept(f);
//		if (f.pre == null)
//			return Collections.emptyList();
//		else
//			return Collections.singletonList(f.pre);
//	}

	/**
	 * Tests if the given node represents a pre-condition declaration
	 * (i.e. a call to {@link Pred#requires(boolean)})
	 * @param node
	 * @return {@code true} if the given node represents a pre-condition
	 */
	public static boolean isPre(MethodInvocation node) {
		IMethodBinding binding = node.resolveMethodBinding();
		return isStaticBoolArgMethod(binding, Pred.class, "requires");
	}

	/**
	 * Tests if the given node represents a post-condition declaration
	 * (i.e. a call to {@link Pred#ensures(boolean)})
	 * @param node
	 * @return {@code true} if the given node represents a post-condition
	 */
	public static boolean isPost(MethodInvocation node) {
		IMethodBinding binding = node.resolveMethodBinding();
		return isStaticBoolArgMethod(binding, Pred.class, "ensures");
	}

	/**
	 * Tests if the given node represents an assumption
	 * (i.e. a call to {@link Pred#assume(boolean)})
	 * @param node
	 * @return {@code true} if the given node represents an assumption
	 */
	public static boolean isAssume(MethodInvocation node) {
		IMethodBinding binding = node.resolveMethodBinding();
		return isStaticBoolArgMethod(binding, Pred.class, "assume");
	}

	/**
	 * Tests if the given node represents a loop invariant declaration
	 * (i.e. a call to {@link Pred#inv(boolean)})
	 * @param node
	 * @return {@code true} if the given node represents a loop invariant
	 */
	private static boolean isInv(MethodInvocation node) {
		IMethodBinding binding = node.resolveMethodBinding();
		return isStaticBoolArgMethod(binding, Pred.class, "inv");
	}

	private static boolean isStaticBoolArgMethod(IMethodBinding binding,
			Class<?> cl, String method) {
		return Modifier.isStatic(binding.getModifiers()) &&
			// no need to check subtyping since we're looking at static method
			binding.getDeclaringClass().getQualifiedName().equals(cl.getName()) &&
			binding.getName().equals(method) &&
			// 1-arg method with boolean argument
			binding.getParameterTypes().length == 1 &&
			binding.getParameterTypes()[0].isPrimitive() &&
			"boolean".equals(binding.getParameterTypes()[0].getName());
	}

	/**
	 * Returns the loop invariant declared in the given loop body
	 * (statement or block), if any
	 * @param loopBody
	 * @return the loop invariant expressions declared in the given loop body, possibly empty
	 */
	public Collection<Expression> getLoopInvariant(Statement loopBody) {
		InvariantFinder f = new InvariantFinder();
		loopBody.accept(f);
		return f.inv == null ? Collections.<Expression>emptyList() : Collections.singletonList(f.inv);
	}

	/**
	 * Set the annotation database to use
	 * @param annos
	 */
	public void setAnnos(AnnotationDatabase annos) {
		this.annos = annos;
	}

	public Contract getContract(ClassInstanceCreation node) {
		return getContract(node, node.resolveConstructorBinding());
	}

	public Contract getContract(MethodInvocation node) {
		return getContract(node, node.resolveMethodBinding());
	}

	public Contract getContract(ConstructorInvocation node) {
		return getContract(node, node.resolveConstructorBinding());
	}

	public Contract getContract(SuperMethodInvocation node) {
		return getContract(node, node.resolveMethodBinding());
	}

	public Contract getContract(SuperConstructorInvocation node) {
		return getContract(node, node.resolveConstructorBinding());
	}

	private Contract getContract(ASTNode node, IMethodBinding target) {
		target = target.getMethodDeclaration();
		Contract result = contracts.get(target);
		if (result == null) {
			MethodDeclaration decl = getMethodSource(target, node);
			if (decl != null)
				result = getContract(decl);
			contracts.put(target, result);
		}
		return result;
	}

	public Contract getContract(MethodDeclaration decl) {
		IMethodBinding binding = decl.resolveBinding();
		Contract result = contracts.get(binding);
		if (result == null) {
			result = createContract(decl);
			contracts.put(binding, result);
		}
		return result;
	}

	@SuppressWarnings("unchecked")
	protected Contract createContract(MethodDeclaration decl) {
		Contract result = new Contract();
		Map<String, Set<IVariableBinding>> modified =
			new LinkedHashMap<String, Set<IVariableBinding>>();

		IMethodBinding method = decl.resolveBinding();
		if (! decl.isConstructor() && ! Modifier.isStatic(decl.getModifiers())) {
			AnnotationSummary summ = annos.getSummaryForMethod(method);
			modified.put(Contract.THIS_VAR_NAME, getModified(
					summ.getReturn(), method.getDeclaringClass()));
		}

		for (SingleVariableDeclaration param : (List<SingleVariableDeclaration>) decl.parameters()) {
			result.addParam(param.getName().getIdentifier());
			IVariableBinding pBinding = param.resolveBinding();
			modified.put(param.getName().getIdentifier(),
					getModified(annos.getAnnosForVariable(pBinding), pBinding.getType()));
		}
		result.setModified(Collections.unmodifiableMap(modified));

		ContractFinder finder = new ContractFinder();
		decl.accept(finder);
		// TODO forbid pre-/post-conditions not supported by permissions
		// (or havoc fields (transitively) not reachable through permissions)
		if (finder.pre != null)
			result.setPre(ExpressionEncoder.encode(finder.pre, SYP_CONTRACT_LOOKUP_INSTANCE, true));
		if (finder.post != null)
			result.setPost(ExpressionEncoder.encode(finder.post, SYP_CONTRACT_LOOKUP_INSTANCE, true));

		return result;
	}

	protected static Set<IVariableBinding> getModified(List<ICrystalAnnotation> annotations,
			ITypeBinding argType) {
		for (ICrystalAnnotation a : annotations) {
			if (Excl.class.getName().equals(a.getName())) {
				Set<IVariableBinding> result = new LinkedHashSet<IVariableBinding>();
				for (Object f : (Object[]) a.getObject("mod")) {
					result.add(resolveField(argType, (String) f));
				}
				return result;
			}
		}
		return null;
	}

	/**
	 * Returns the variable binding for the given field descriptor
	 * relative to the given object type or {@code null} if the field
	 * descriptor denotes the contents of an array
	 * @param objType Object type relative to which {@code field} is resolved
	 * @param field field name, {@code super.} plus field name or
	 * an array content descriptor, currently only [*]
	 * @return the variable binding for the given field descriptor
	 * or {@code null} for the contents of an array
	 */
	static IVariableBinding resolveField(ITypeBinding objType, String field) {
		if (field.startsWith(SUPER_PREFIX)) {
			objType = objType.getSuperclass();
			field = field.substring(SUPER_PREFIX.length());
		}
		if (field.contains("."))
			throw new IllegalArgumentException("Transitive fields not needed: " + field);
		if (field.startsWith("[")) {
			if ("[*]".equals(field))
				// array contents--no variable binding, use null marker
				return null;
			// theoretically we could support [5] or [][*] here
			// but we have no way of encoding that right now
			// as we use variable bindings in the return type
			throw new UnsupportedOperationException(
					"Unsupported array modifier: " + field);
		}
		if (objType != null) {
			for (IVariableBinding f : objType.getDeclaredFields()) {
				if (f.getName().equals(field))
					return f;
			}
		}
		throw new IllegalArgumentException("Unknown field: " + field);
	}

	/** Assumes that name is defined in same comp unit */
	private static Expression getInitializer(SimpleName name) {
		VariableInitFinder f = new VariableInitFinder();
		f.needed = (IVariableBinding) name.resolveBinding();
		name.getRoot().accept(f);
		return f.result;
	}

	/**
	 * Returns the class invariants declared for the given type node,
	 * including (visible) invariants declared in super-types
	 * @param clazz never {@code null}
	 * @return the visible class invariants declared for the given type
	 * @see IChecker#getInvariants(TypeDeclaration)
	 */
	public Collection<Expression> getInvariants(TypeDeclaration clazz) {
		Map<ITypeBinding, Expression> result;
		ITypeBinding binding = clazz.resolveBinding();
		if (binding.getSuperclass() == null)
			// no invariant for java.lang.Object (don't expect to have source)
			result = getInvariants(binding, clazz);
		else
			result = getInvariants(binding.getSuperclass(), clazz);
		for (MethodDeclaration m : clazz.getMethods()) {
			// look for inv() method
			if ("inv".equals(m.getName().getIdentifier()) &&
					m.parameters().isEmpty()) {
				ReturnStatement r = ReturnFinder.findReturn(m);
				if (r != null && r.getExpression() != null)
					result.put(binding, r.getExpression());
				else
					throw new NullPointerException("Unexpected null: " + r);
			}
		}
		return result.values();
	}

	/**
	 * Returns the class invariants declared for the given type binding,
	 * including (visible) invariants declared in super-types
	 * @param clazz never {@code null}
	 * @return the visible class invariants declared for the given type
	 * @see IChecker#getInvariants(ITypeBinding)
	 */
	public Collection<Expression> getInvariants(ITypeBinding clazz) {
		return getInvariants(clazz, null).values();
	}

	private static Map<ITypeBinding, Expression> getInvariants(ITypeBinding clazz, ASTNode hint) {
		Map<ITypeBinding, Expression> result;
		if (clazz.getSuperclass() == null)
			// no invariant for java.lang.Object
			result = new LinkedHashMap<ITypeBinding, Expression>();
		else
			result = getInvariants(clazz.getSuperclass(), hint);
		for (IMethodBinding m : clazz.getDeclaredMethods()) {
			// check if there is even an inv() method defined before parsing
			if ("inv".equals(m.getName()) &&
					m.getParameterTypes().length == 0 &&
					"boolean".equals(m.getReturnType().getName())) {
				MethodDeclaration decl = getMethodSource(m, hint);
				ReturnStatement r = ReturnFinder.findReturn(decl);
				if (r != null && r.getExpression() != null)
					result.put(clazz, r.getExpression());
				else
					throw new NullPointerException("Unexpected null: " + r);
				break; // found it!
			}
		}
		return result;
	}

	/**
	 * @param target Method whose source is to be returned
	 * @param invocation may be <code>null</code> but avoids parsing if {@code target}
	 * is in the same compilation unit as {@code invocation}
	 * @return an AST with bindings for {@code target}, which may not have a
	 * body if the method is abstract
	 */
	private static MethodDeclaration getMethodSource(IMethodBinding target, ASTNode invocation) {
		CompilationUnit root = getSource(target, invocation);
		if (root == null)
			return null;
		MethodFinder finder = new MethodFinder();
		finder.needed = target;
		root.accept(finder);
		return finder.result;
	}

	/**
	 * @param target Method whose source is to be returned
	 * @param invocation may be <code>null</code> but avoids parsing if {@code target}
	 * is in the same compilation unit as {@code invocation}
	 * @return an AST with bindings for {@code target}, which may not have a
	 * body if the method is abstract
	 */
	protected static CompilationUnit getSource(IBinding target, ASTNode hint) {
		CompilationUnit root = hint == null ? null : (CompilationUnit) hint.getRoot();
		IJavaElement targetElement = target.getJavaElement();
		if (targetElement == null)
			return null; // synthetic element (like implicit constructor), so no source
		IJavaElement rootElement = root == null ? null : root.getJavaElement();
		if (root == null || rootElement == null ||
				rootElement.getResource() == null /* root is in external archive */ ||
				! (rootElement instanceof ICompilationUnit &&
						rootElement.getResource().equals(
								targetElement.getResource())))
		{
			// find comp unit or class file the target is in
			while (! (targetElement instanceof ITypeRoot)) {
				targetElement = targetElement.getParent();
				if (targetElement == null)
					// shouldn't happen but catch this anyway
					return null;
			}
			// resources are reliable for telling compilation units apart
			// but not class files because their resource is null (for external
			// archives like the standard library) or the archive they are in
			// (so two different class files can share the same resource)
			// hence check if we ended up with same type root before parsing
			if (rootElement != targetElement) {
				ASTParser parser = ASTParser.newParser(AST.JLS3);
				parser.setSource((ITypeRoot) targetElement);
				parser.setResolveBindings(true);
				parser.setBindingsRecovery(true);
				try {
					root = (CompilationUnit) parser.createAST(null /* no progress monitor */);
				} catch (IllegalStateException e) {
					// parsing problems
					// this would in particular happen if targetElement
					// is a class file with no associated source
					return null;
				}
			} // otherwise root and target are the same class file
			// TODO cache ASTs so we don't have to parse the same comp unit over and over
		} // else target is in the same comp unit as the invocation...
		return root;
	}

	/**
	 * This class must not have or modify any state!
	 * @author kevin
	 * @since Feb 13, 2011
	 */
	private static class SypContractLookup implements Lookup {

		@Override
		public Field getField(Ref accessor, IVariableBinding field) {
			if (accessor == null)
				// FIXME resolve implicit this...
				accessor = new Local(Contract.THIS_VAR_NAME, field.getDeclaringClass());
			return new Field(accessor, field);
		}

		@Override
		public Ref getName(Expression e) {
			if (e instanceof SimpleName) {
				SimpleName name = (SimpleName) e;
				IVariableBinding var = (IVariableBinding) name.resolveBinding();
				if (var.isField())
					return getField(null, var);
				else if (var.isEnumConstant())
					return null;
				// else local...

				for (IAnnotationBinding a : var.getAnnotations()) {
					if (Result.class.getName().equals(a.getAnnotationType().getQualifiedName())) {
						// TODO ensure final variable
						return new Local(Contract.RESULT_VAR_NAME, var.getType());
					}
					else if (Old.class.getName().equals(a.getAnnotationType().getQualifiedName())) {
//						// TODO ensure final variable
						int dim = 0;
						for (IMemberValuePairBinding p : a.getAllMemberValuePairs()) {
							if ("dim".equals(p.getName()))
								dim = (Integer) p.getValue();
						}
						// will peel dimensions > 0 off in getSelect
						Expression init = getInitializer(name);
						if (init instanceof MethodInvocation) {
							if (dim == 0)
								throw new IllegalStateException("Field pre-image must be initialized with field value");
							MethodInvocation invocation = (MethodInvocation) init;
							IMethodBinding m = invocation.resolveMethodBinding();
							// grr, Java's name is ...Old$Arrays but Eclipse's is ...Old.Arrays
							if (! Old.Arrays.class.getName().replace('$', '.').equals(m.getDeclaringClass().getQualifiedName()))
								throw new UnsupportedOperationException(
										"Invocations not supported in Old initializers");
							int copyDepth = 1;
							if (1 < invocation.arguments().size())
								copyDepth = (Integer) ((NumberLiteral) invocation.arguments().get(1)).resolveConstantExpressionValue();
							if (copyDepth != dim)
								throw new IllegalStateException("declared pre-image dimension " + dim +
										" doesn't correspond to actual: " + copyDepth);
							init = (Expression) invocation.arguments().get(0);
						}
						return new Pre((Ref) ExpressionEncoder.encode(init, this), dim);
					}
				}
				// not a local with @Result or @Old annotation, so must be a parameter
				if (! var.isParameter())
					throw new IllegalArgumentException("Cannot use local variable in contract: " + e);
				return new Local(var);
			}
			if (e instanceof QualifiedName) {
				QualifiedName f = (QualifiedName) e;
				Ref access = getName(f.getQualifier());
				return getField(access, (IVariableBinding) f.resolveBinding());
			}
			if (e instanceof FieldAccess) {
				FieldAccess f = (FieldAccess) e;
				Ref access = getName(f.getExpression());
				return getField(access, f.resolveFieldBinding());
			}
			if (e instanceof ParenthesizedExpression)
				return getName(((ParenthesizedExpression) e).getExpression());
			if (e instanceof ThisExpression)
				return new Local(e.toString(), ((ThisExpression) e).resolveTypeBinding());
			throw new IllegalArgumentException("Not a variable: " + e);
		}

		@Override
		public Ref getSelect(Formula array, Formula index,
				ITypeBinding elementType) {
			if (array instanceof Pre) {
				Pre old = (Pre) array;
				if (0 < old.getArrayDim()) {
					return new Pre(new Select(old.getAged(), index, elementType),
							old.getArrayDim() - 1);
				}
			}
			return new Select(array, index, elementType);
		}
	}

	private static class MethodFinder extends ASTVisitor {

		IMethodBinding needed;
		MethodDeclaration result;

		@Override
		public boolean visit(MethodDeclaration node) {
			IMethodBinding binding = node.resolveBinding();
			// normally binding and binding.getJavaElement should be non-null
			// but we had unfortunate incidents in the presence of build errors
			if (binding == null)
				return true;
			if (binding.equals(needed) ||
					(binding.getJavaElement() != null && binding.getJavaElement().equals(needed.getJavaElement()))) {
				if (result != null)
					throw new IllegalStateException("Method found twice: " + node);
				result = node;
				return false;
			}
			// catch anonymous inner classes...
			return true;
		}
	}

	private static class VariableInitFinder extends ASTVisitor {

		IVariableBinding needed;
		Expression result;

		@Override
		public boolean visit(Assignment node) {
			Expression lhs = node.getLeftHandSide();
			if (lhs instanceof SimpleName && ((SimpleName) lhs).resolveBinding().equals(needed)) {
				if (result != null)
					throw new IllegalStateException("Variable initialized twice: " + node);
				result = node.getRightHandSide();
			}
			return true;
		}

		@Override
		public boolean visit(SingleVariableDeclaration node) {
			return visitDecl(node);
		}

		@Override
		public boolean visit(VariableDeclarationFragment node) {
			return visitDecl(node);
		}

		private boolean visitDecl(VariableDeclaration node) {
			if (node.resolveBinding().equals(needed) && node.getInitializer() != null) {
				if (result != null)
					throw new IllegalStateException("Variable initialized twice: " + node);
				result = node.getInitializer();
				return false;
			}
			// catch anonymous inner classes...
			return true;
		}
	}

	private static class ContractFinder extends ASTVisitor {

		Expression pre;
		Expression post;
		private boolean inMethod = false;

		@Override
		public boolean visit(MethodDeclaration node) {
			// do not descend into nested methods
			if (inMethod)
				return false;
			inMethod = true;
			return true;
		}

		@Override
		public void endVisit(MethodInvocation node) {
			if (ContractRegistry.isPre(node)) {
				if (pre == null)
					pre = (Expression) node.arguments().get(0);
				else
					throw new IllegalStateException("Multiple pre-conditions: " + node);
			}
			if (ContractRegistry.isPost(node)) {
				if (post == null)
					post = (Expression) node.arguments().get(0);
				else
					throw new IllegalStateException("Multiple post-conditions: " + node);
			}
		}
	}

	private static class InvariantFinder extends ASTVisitor {

		Expression inv;

		@Override
		public void endVisit(MethodInvocation node) {
			if (ContractRegistry.isInv(node)) {
				if (inv == null)
					inv = (Expression) node.arguments().get(0);
				else
					throw new IllegalStateException("Multiple invariants: " + node);
			}
		}

		@Override
		public boolean visit(DoStatement node) {
			return false;
		}

		@Override
		public boolean visit(EnhancedForStatement node) {
			return false;
		}

		@Override
		public boolean visit(ForStatement node) {
			return false;
		}

		@Override
		public boolean visit(WhileStatement node) {
			return false;
		}
	}
}
